Nuprl Lemma : fpf-normalize_wf 11,40
A:Type, eq:EqDecider(A), B:(AType), g:x:A fp B(x). fpf-normalize(eq;g)  x:A fp B(x) 
latex

Definitionst  T, f(a), x(s), x.A(x), x. t(x), x:A. B(x), , (x  l), {x:A| B(x)} , a:A fp B(a), x:AB(x), x : v, f  g, reduce(f;k;as), fpf-normalize(eq;g), x:A  B(x), Type, EqDecider(T)
Lemmasdeq wf, list-subtype, reduce wf, fpf-join wf, fpf-single wf, fpf wf, l member wf, fpf-empty wf

origin